load("@rules_rust//rust:defs.bzl", "rust_library", "rust_proc_macro", "rust_test")

package(default_visibility = ["//visibility:public"])

rust_library(
    name = "tla_instrumentation",
    srcs = glob(["tla_instrumentation/src/**/*.rs"]),
    crate_name = "tla_instrumentation",
    deps = [
        "@crate_index//:candid",
        "@crate_index//:serde",
        "@crate_index//:sha2",
        "@crate_index//:uuid",
    ],
)

rust_library(
    name = "local_key",
    srcs = glob(["local_key/src/**/*.rs"]),
    crate_name = "local_key",
    deps = [
        "@crate_index//:pin-project-lite",
    ],
)

rust_test(
    name = "structs_test",
    srcs = [
        "tla_instrumentation/tests/common.rs",
        "tla_instrumentation/tests/structs.rs",
    ],
    crate_root = "tla_instrumentation/tests/structs.rs",
    data = [
        ":tla_models",
        "@bazel_tools//tools/jdk:current_java_runtime",
        "@tla_apalache//:bin/apalache-mc",
    ],
    env = {
        "JAVABASE": "$(JAVABASE)",
        "TLA_APALACHE_BIN": "$(rootpath @tla_apalache//:bin/apalache-mc)",
        "TLA_MODULES": "$(locations :tla_models)",
    },
    proc_macro_deps = [
        ":proc_macros",
        "@crate_index//:async-trait",
    ],
    toolchains = ["@bazel_tools//tools/jdk:current_java_runtime"],
    deps = [
        ":local_key",
        ":tla_instrumentation",
        "@crate_index//:candid",
        "@crate_index//:tokio-test",
    ],
)

rust_test(
    name = "basic_tests",
    srcs = ["tla_instrumentation/tests/basic_tests.rs"],
    deps = [":tla_instrumentation"],
)

rust_test(
    name = "args_test",
    srcs = [
        "tla_instrumentation/tests/args_test.rs",
        "tla_instrumentation/tests/common.rs",
    ],
    crate_root = "tla_instrumentation/tests/args_test.rs",
    data = [
        ":tla_models",
        "@bazel_tools//tools/jdk:current_java_runtime",
        "@tla_apalache//:bin/apalache-mc",
    ],
    env = {
        "JAVABASE": "$(JAVABASE)",
        "TLA_APALACHE_BIN": "$(rootpath @tla_apalache//:bin/apalache-mc)",
        "TLA_MODULES": "$(locations :tla_models)",
    },
    proc_macro_deps = [
        ":proc_macros",
        "@crate_index//:async-trait",
    ],
    toolchains = ["@bazel_tools//tools/jdk:current_java_runtime"],
    deps = [
        ":local_key",
        ":tla_instrumentation",
        "@crate_index//:candid",
        "@crate_index//:tokio-test",
    ],
)

rust_test(
    name = "multiple_calls_test",
    srcs = [
        "tla_instrumentation/tests/common.rs",
        "tla_instrumentation/tests/multiple_calls.rs",
    ],
    crate_root = "tla_instrumentation/tests/multiple_calls.rs",
    data = [
        ":tla_models",
        "@bazel_tools//tools/jdk:current_java_runtime",
        "@tla_apalache//:bin/apalache-mc",
    ],
    env = {
        "JAVABASE": "$(JAVABASE)",
        "TLA_APALACHE_BIN": "$(rootpath @tla_apalache//:bin/apalache-mc)",
        "TLA_MODULES": "$(locations :tla_models)",
    },
    proc_macro_deps = [
        ":proc_macros",
        "@crate_index//:async-trait",
    ],
    toolchains = ["@bazel_tools//tools/jdk:current_java_runtime"],
    deps = [
        ":local_key",
        ":tla_instrumentation",
        "@crate_index//:candid",
        "@crate_index//:tokio-test",
    ],
)

# all TLA mdels
# NOTE: the test runner assumes unique basenames
filegroup(
    name = "tla_models",
    srcs = glob(["tla/*.tla"]),
)

rust_proc_macro(
    name = "proc_macros",
    srcs = glob(["tla_instrumentation_proc_macros/src/**/*.rs"]),
    crate_name = "tla_instrumentation_proc_macros",
    deps = [
        "@crate_index//:proc-macro2",
        "@crate_index//:quote",
        "@crate_index//:syn",
    ],
)
